T:Type, as, bs, cs:T List. as @ bs  as @ cs  bs  cs 

latex

Definitions	t  T, x:A. B(x), as @ bs, Prop, x:A. B(x), P  Q, P  Q, P & Q, P  Q, l1  l2, ||as||
Lemmas	append assoc, append-cancellation, length wf1, append wf